COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 lispax.lsp[f81,jmc]	ekl axioms for lisp
C00008 00003
C00010 ENDMK
C⊗;
;;; lispax.lsp[f81,jmc]	ekl axioms for lisp

(proof lispax)

(DECL (U u0 u1 u2 u3 v v0 v1 v2 v3 W w0 w1 w2 w3) |ground| variable listp)

(DECL (X Y Z) |GROUND| VARIABLE sEXP)

(DECL (A B C) |GROUND| VARIABLE)

(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)

(DECL (NNIL) |GROUND| CONsTANT LIsTp)

(DECL (CONs) |GROUND⊗GROUND→GROUND| CONsTANT)

(DECL (CAR CDR) |GROUND→GROUND| CONsTANT nil unary 950)

(DECL (NULL) |GROUND→TRUTHVAL| CONsTANT nil unary 750)

(DECL (LIsTp) |GROUND→TRUTHVAL| CONsTANT nil unary 750)

(DECL (sEXP) |GROUND→TRUTHVAL| CONsTANT nil unary 750)

(AXIOM |∀U.sEXP U |)

(AXIOM |∀X U.LIsTp CONs(X,U) |)

(AXIOM |∀U.NULL U ≡ U=NNIL|)

(AXIOM |∀X U.¬NULL CONs(X,U)|)

(AXIOM |∀X U.CAR CONs(X,U) =X|)

(AXIOM |∀X U.CDR CONs(X,U) = U|)

(AXIOM |∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(CONs(X,U)))⊃(∀U.PHI(U))|)

;;; Common defined functions

(DECL (*) |GROUND⊗GROUND→GROUND| CONsTANT NIL INFIX 840)

(axiom |∀u v.listp(u*v)|)

(AXIOM |∀U V.(U*V)=IF NULL(U) THEN V ELsE CONs(CAR(U),CDR(U)*V)|)

(decl (reverse) |ground→ground| constant nil unary 950)

(decl list |ground* → ground| functional)

(axiom |∀x.listp(list(x))|)

(axiom |∀x.list(x) = cons(x,nnil)|)

(axiom |∀x y.listp(list(x,y))|)

(axiom |∀x y.list(x,y) = cons(x,list(y))|)

(axiom |∀x y z.listp(list(x,y,z))|)

(axiom |∀x y z.list(x,y,z) = cons(x,list(y,z))|)

(axiom |∀u.listp(reverse(u))|)

(axiom |∀u.reverse(u) = if null(u) then nnil
else reverse(cdr(u)) * list(car(u))|)

;;; theorems taken as axioms for further proofs

(axiom |∀u v w.(u*v)*w = u*(v*w)|)

(axiom |∀x u v.cons(x,u*v) = cons(x,u)*v|)

(axiom |∀u v.reverse(u*v) = reverse v * reverse u|)
LISPAX started.
* 
* 
* 
* 
* 
* 
* 
* 
* 
* 
* 11. ∀U.SEXP U
    ctxt: (1 10)   deps: NIL

* 12. ∀X U.LISTP CONS(X,U)
    ctxt: (1 2 6 9)   deps: NIL

* 13. ∀U.NULL U≡U=NNIL
    ctxt: (1 5 8)   deps: NIL

* 14. ∀X U.¬NULL CONS(X,U)
    ctxt: (1 2 6 8)   deps: NIL

* 15. ∀X U.CAR CONS(X,U)=X
    ctxt: (1 2 6 7)   deps: NIL

* 16. ∀X U.CDR CONS(X,U)=U
    ctxt: (1 2 6 7)   deps: NIL

* 17. ∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(CONS(X,U)))⊃(∀U.PHI(U))
    ctxt: (1 2 4 5 6)   deps: NIL

* 
* 19. ∀U V.LISTP U*V
    ctxt: (1 9 18)   deps: NIL

* 20. ∀U V.U*V=IF NULL U THEN V ELSE CONS(CAR U,CDR U*V)
    ctxt: (1 6 7 8 18)   deps: NIL

* 
* 
* 23. ∀X.LISTP LIST(X)
    ctxt: (2 9 22)   deps: NIL

* 24. ∀X.LIST(X)=CONS(X,NNIL)
    ctxt: (2 5 6 22)   deps: NIL

* 25. ∀X Y.LISTP LIST(X,Y)
    ctxt: (2 9 22)   deps: NIL

* 26. ∀X Y.LIST(X,Y)=CONS(X,LIST(Y))
    ctxt: (2 6 22)   deps: NIL

* 27. ∀X Y Z.LISTP LIST(X,Y,Z)
    ctxt: (2 9 22)   deps: NIL

* 28. ∀X Y Z.LIST(X,Y,Z)=CONS(X,LIST(Y,Z))
    ctxt: (2 6 22)   deps: NIL

* 29. ∀U.LISTP REVERSE U
    ctxt: (1 9 21)   deps: NIL

* 30. ∀U.REVERSE U=IF NULL U THEN NNIL ELSE REVERSE (CDR U)*LIST(CAR U)
    ctxt: (1 5 7 8 18 21 22)   deps: NIL

* 31. ∀U V W.(U*V)*W=U*(V*W)
    ctxt: (1 18)   deps: NIL

* 32. ∀X U V.CONS(X,U*V)=CONS(X,U)*V
    ctxt: (1 2 6 18)   deps: NIL

* 33. ∀U V.REVERSE (U*V)=REVERSE V*REVERSE U
    ctxt: (1 18 21)   deps: NIL

* 
(assume |v1=reverse u1|)
34. V1=REVERSE U1
    ctxt: (1 21)   deps: (34)

(assume |x=reverse u1|)
35. X=REVERSE U1
    ctxt: (1 2 21)   deps: (35)

(decsimp |listp x| nil (35 29) nil nil (35 29))
o.k.
* 36. LISTP X
(deletel 34:*)

* done.
*